a, b:. Dec(a < b) 

latex

Definitions	qpositive(r), b, P  Q, P & Q, T, P  Q, r - s, i <z j, True, b, ff, if b then t else f fi , tt, p q, p  q, , {T}, P  Q, SQType(T), t.1, q_le(r;s), t.2, , , x f y, gset, a < b, goset, a <p b, <+>, a < b, t  T, r < s, x:A. B(x), A, False, Unit, , S  T,
Lemmas	member-decide-assert, bfalse wf, qadd comm q, qinv inv q, qadd wf, qmul over plus qrng, qmul wf, int inc rationals, btrue wf, qinverse q, true wf, squash wf, not functionality wrt iff, assert-qeq, qminus positive, assert of bnot, eqff to assert, not wf, assert wf, iff transitivity, eqtt to assert, bnot wf, qeq wf2, qsub wf, qpositive wf, bor wf, band wf, bool wf, bool sq, rationals wf